Nuprl Lemma : fpf-val-single1
0,22
postcript
pdf
A
:Type,
eq
:EqDecider(
A
),
x
:
A
,
v
,
P
:Top. (
z
!=
x
:
v
(
x
)
P
(
a
,
z
)) ~ (True
P
(
x
,
v
))
latex
Definitions
f
(
x
)
,
,
eqof(
d
)
,
true
,
Top
,
EqDecider(
T
)
,
x
:
v
,
z
!=
f
(
x
)
P
(
a
;
z
)
,
x
dom(
f
)
,
b
,
Prop
,
SQType(
T
)
,
P
Q
,
{
T
}
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
btrue
wf
,
eqof
wf
,
bool
sq
,
bool
wf
,
deq
wf
,
top
wf
,
eqof
eq
btrue
origin
A:Type, eq:EqDecider(A), x:A, v, P:Top. (z != x : v(x) 
P(a,z)) ~ (True P(x,v)) A:Type, eq:EqDecider(A), x:A, v, P:Top. (z != x : v(x) P(a,z)) ~ (True P(x,v)) 
P(a;z)
dom(f)
b Q Tx:A. B(x)